#include "ic3.h"
#include "minisat-2.2/mtl/Sort.h"
static unsigned NCTRLVAR = 30;

/////////////////////////////
//  STATIC LOCAL FUNCTION 
//

/// state to refutate clause c = ~s 
void state2clause( const State s , unsigned ns , Minisat::Lit * x , Minisat::Lit * lit )
{
   for( uint64_t i=0 , j=0 , k=1 ; i < ns ; ((++i)&0x3F) ? (k+=k) : (k=1,j+=1) )
      x[i] = ( s[j] & k ) ? ~lit[i] : lit[i];
}
/// state to next frame assumptions ( vector of unit clause )
void state2nstate( const State s , unsigned ns , Minisat::Lit * x , Minisat::Lit * lit )
{
   for( uint64_t i=0 , j=0 , k=1 ; i < ns ; ((++i)&0x3F) ? (k+=k) : (k=1,j+=1) )
      x[i] =  ( s[j] & k ) ? lit[i+ns] : ~lit[i+ns];
}
/// clause to next time frame (a+b+c) -> (~a) (~b) (~c)
void clause2nstate( const Clause & y , unsigned ns , Clause & x , Minisat::Lit * lit)
{
   assert( x.size() == y.size() );
   for( int i = 0 ; i < y.size() ; ++i )
      x[i] = lit[ var(y[i]) + ns ] ^ sign(y[i]) ^ 1;
}
// next frame clause to claues 
void nclause2clause( const Clause & y , Clause & x , Minisat::Lit * rev)
{
   assert( x.size() == y.size() );
   for( int i = 0 ; i < y.size() ; ++i )
      x[i] = rev[var(y[i])] ^ sign(y[i]);
}
void nstate2clause( const Clause & y , Clause & x , Minisat::Lit * rev )
{
   assert( x.size() == y.size() );
   for( int i = 0 ; i < y.size() ; ++i )
      x[i] = rev[var(y[i])] ^ sign(y[i]) ^1;
}

static unsigned witsat=0;
static unsigned progsat=0;
static unsigned invtest=0;
static unsigned downsat=0;
static unsigned upsat =0;
#define PRINT( a , b ) std::cout<<#a<<"\t[ "<<b<< " ] " <<std::endl;
void print_prof() 
{
   std::cout << " ===== PROFILING ===== "<< std::endl;
   PRINT( witness sat    , witsat );
   PRINT( propagate sat  , progsat );
   PRINT( invariant test , invtest );
   PRINT( down algo sat , downsat );
   PRINT( up algo sat , upsat );
   PRINT( total sat , witsat+progsat+invtest+downsat+upsat );
   std::cout << " ===================== "<< std::endl;
}

/////////////////////////////////
// Minisat IC3 Implementation 
//
MinisatIC3::MinisatIC3( vec< Clause > & c , IC3Param & p )
   : IC3Param( p ) , _uctrl(0)
{
   for( unsigned i = 0 ; i < _nvar + NCTRLVAR ; ++ i ) // additional variable 
      newVar();
   for( unsigned i = 0 ; i < c.size() ; ++ i )
      addClause( c[i] );
}
/// for hunting witness
bool MinisatIC3::sat()
{
   witsat+=1;
   return solve( ~_lits[_nstates<<1] );
}
/// for propagate clause 
bool MinisatIC3::sat( const Clause & c )
{
   progsat+=1;
   Clause x( c.size() );
   clause2nstate( c , _nstates , x , _lits );
   return solve( x );
}
/// for evaluate invariant 
bool MinisatIC3::sat( const State s )
{
   invtest+=1;
   Minisat::Lit ctrl = get_ctrl();

   Clause x(_nstates+1) , y(_nstates+1);
   state2clause( s , _nstates , x.data , _lits ); x[ _nstates ] = ctrl;
   y[0] = ~ctrl; state2nstate( s , _nstates , y.data + 1 , _lits );

   addClause( x );
   bool ret = solve( y );
   addClause( ctrl );
   return ret;
}
/// witness from model valut --> could be enhance as tri-state sim
void MinisatIC3::witness( State s )
{
   for( uint64_t i=0 , j=0 , k=1 ; i < _nstates ; ((++i)&0x3F) ? (k+=k) : (k=1,j+=1) )
      if( modelValue( i )==Minisat::l_True ) 
         s[j]|=k;
      else
         s[j]&=(~k);
}
static void drop( const Clause & c , unsigned t , Clause & d )
{
   for( unsigned i=0 , k=0; i < (unsigned)c.size() ; ++i ){
      if( t == i ) continue;
      d[k++] = c[i];
   }
}
static void copyTo( const Clause & c , Clause & d ){
   //d.resize( c.size() );
   d.clear();d.growTo(c.size());
   for( int i = 0 ; i < c.size() ; ++i )
      d[i] = c[i];
}
bool init( Clause & c )
{
   for( int i = 0 ; i < c.size() ; ++i )
      if( sign(c[i]) == true )return true;
   return false;
}
/// prove F&T&c -> ~c'
bool MinisatIC3::consecution( Clause & c )
{
   downsat+=1;
   Minisat::Lit ctrl = get_ctrl();
   Clause a( c.size() );
   
   clause2nstate( c , _nstates , a , _lits );
   c.push( ctrl ) ; a.push( ~ctrl );

   addClause( c ); c.pop();
   bool ret = solve( a );
   addClause( ctrl );
   return ret == false;
}
/// kinds of tail recursive
bool MinisatIC3::MIC( Clause & c )
{
   if( DOWN( c ) == false ) return false;

   UP( c );
   unsigned sz = c.size();
   Clause d(sz-1);
   for( unsigned i = 0 ; i < sz ; ++ i )
   {
      d.growTo( sz -1  );
      drop( c , i , d );
      if( MIC( d ) )
      {
         copyTo( d , c );
         return true;
      }
   }
   return true;
}

bool MinisatIC3::DOWN( Clause & c )
{
   if( init( c ) == false ) 
      return false;
   if( consecution( c ) ) return true;
  
   // tri-state simulation, leaving the control variable 
   int k = 0;
   for( int i = 0 ; i < c.size() ; ++ i )
      if( modelValue( c[i] ) == Minisat::l_False )
         c[k++] = c[i];
   c.sz = k ;

   // unclude negtive literal 
   return DOWN( c );
}
uint8_t inC[100000]={0};
static void conjunct( const Clause & c , Clause & s )
{
   for( int i = 0 ; i < c.size() ; ++ i ) inC[ var(c[i]) ] = true;
   int k = 0;
   for( int i = 0 ; i < s.size() ; ++ i )
      if( inC[ var(s[i] ) ] )
         s[k++] = s[i];
   s.sz = k;
   for( int i = 0 ; i < c.size() ; ++ i ) inC[ var(c[i]) ] = false;
}
static void split( const Clause & s0 , Clause & l , Clause & r)
{
   unsigned s = s0.size()/2;
   l.growTo( s + s0.size()%2 ); r.growTo( s );
   for( int i = 0 ; i < s0.size() ; ++i )
      if( i%2 )r[i>>1] = s0[i];
      else     l[i>>1] = s0[i];
}
static void add( const Clause & a , const Clause & b , Minisat::Lit ctrl , Clause & o )
{
   o.clear(); o.growTo( a.size() + b.size() + 1 );
   int k = 0 ;
   for( int i = 0 ; i < a.size() ; ++ i ) o[k++] = a[i];
   for( int i = 0 ; i < b.size() ; ++ i ) o[k++] = b[i];
   o[k] = ctrl;
}
static void add( const Clause & a , const Clause & b , Clause & o )
{
   o.clear();o.growTo( a.size() + b.size() );
   int k = 0 ;
   for( int i = 0 ; i < a.size() ; ++ i ) o[k++] = a[i];
   for( int i = 0 ; i < b.size() ; ++ i ) o[k++] = b[i];
}
static void disjoint( const Clause & a, const Clause & b, Clause & c )
{
   c.clear(); c.growTo( a.size() );
   for( int i = 0 ; i < a.size() ; ++ i )c[i]=a[i] , inC[ var(a[i]) ] = true;
   for( int i = 0 ; i < b.size() ; ++ i )
      if( inC[ var(b[i]) ] == false ) 
         c.push( b[i] );
   for( int i = 0 ; i < a.size() ; ++i ) inC[var(a[i])] = false;

}
void MinisatIC3::min_opt_rec( Clause & sup , Clause & s0 , Minisat::Lit ctrl )
{
   if( s0.size() == 1 ) return ;

   Clause l0, r0; split( s0 , l0 , r0 );
   Clause C; 

   add( sup , l0 , ~ctrl , C );
   upsat+=1;
   if( solve( C ) == false)
   {
      conjunct( conflict , sup );
      conjunct( conflict , l0 );
      min_opt_rec( sup , l0 , ctrl );
      for( int i = 0 ; i < l0.size() ; ++i )s0[i]=l0[i];
      s0.sz = l0.sz;
      return;
   }

   add( sup , r0 , ~ctrl , C );
   upsat+=1;
   if( solve( C ) == false )
   {
      conjunct( conflict , sup );
      conjunct( conflict , r0 );
      min_opt_rec( sup , r0 , ctrl  );
      for( int i = 0 ; i < r0.size() ; ++i )s0[i]=r0[i];
      s0.sz = r0.sz;
      return;
   }
   
   add( sup , r0 , C );
   min_opt_rec( C , l0 , ctrl );
   conjunct( C , sup );
   conjunct( C , r0 );
   add( sup , l0 , C );
   min_opt_rec( C , r0 , ctrl );
   conjunct( C, sup );
   conjunct( C, l0 );
   //disjoint( l0 , r0 , s0 );
   add( l0 , r0 , s0 );
}
void MinisatIC3::min_opt( Clause & a , Minisat::Lit ctrl )
{
   Clause tmp;
   min_opt_rec( tmp , a , ctrl );
}
void MinisatIC3::min( Clause & a , Minisat::Lit ctrl )
{
   for( int i = a.size()-1 ; i >= 0 ; -- i )
   {    
      Minisat::Lit tmp = a[i];
      a[i] = ~ctrl;

      upsat+=1;
      if( solve( a ) == false )
      {
         for( int j = i ; j < a.size()-1 ; ++ j )
            a[j] = a[j+1];
         a.shrink(1);
      }else a[i] = tmp;
   }
}
bool MinisatIC3::implicate( Clause & c , Clause & c0 , uint8_t * mark )
{
   Minisat::Lit ctrl = get_ctrl();
   c.push( ctrl );
   addClause( c );
   c.pop();
   
   Clause a( c0.size() );
   clause2nstate( c0 , _nstates , a , _lits );
   min_opt( a , ctrl );
   addClause( ctrl ); 

   bool contain = true;
   for( int i = 0 ; i < a.size() ; ++ i )
   {
      unsigned v = var(_rlits[ var(a[i]) ]);
      if( mark[ v ] == false )
      {
         mark[v] = true;
         contain = false;
         c.push( _rlits[var(a[i])] ^ sign(a[i]) ^ 1);
      }
   }

   if( contain == true ){ c0.clear() ; c0.growTo(c.size() ); copyTo( c , c0 ); }
   return contain;
}
void MinisatIC3::UP( Clause & c0 )
{
   Clause c(c0.size());c.clear();

   uint8_t mark[ _nstates ];
   memset( mark , 0 , sizeof(uint8_t)*_nstates );

   for( int i = 0 ; i < c0.size() ; ++ i )
      if( sign(c0[i]) == true ) // no break have better result 
         c.push( c0[i] ) , mark[ var(c0[i]) ] = true;

   while( implicate( c , c0 , mark ) == false );
   
}
/// temporary usage function at subclause inductive relative 
static bool valid( Clause & c , int nvar)
{
   for( int i = 0 ; i < c.size() ; ++i )
      if( var( c[i] ) >= nvar ) return false;
   return true;
}
// TODO make sure the solve solved sat  
void MinisatIC3::subclause_inductive_relative( const State s , Clause & c )
{
   assert( sat(s) == false );

   if( var( conflict.last() ) >= ((int)_nvar) ) conflict.pop();
   assert( valid(conflict , _nvar ) );

   c.growTo( conflict.size() );
   nclause2clause( conflict , c , _rlits );

   if( init(c) == false )
   { 
      uint64_t j = 0 , k = 1;
      for( unsigned i = 0 ; i < _nstates ; ++ i )
      {
         if( s[j] & k ){ c.push( ~_lits[i] ); break ;}
         if( (i & 0x3F) == 0x3F ) j +=1 , k = 1;
         else k = k << 1;
      }
   }

   MIC( c );
   Minisat::sort(c);
}

Minisat::Lit MinisatIC3::get_ctrl()
{
   if( _uctrl == NCTRLVAR )recycle();
   return Minisat::mkLit( _nvar + _uctrl++ , 0 );
}
void MinisatIC3::recycle()
{
   removeSatisfied( learnts );
   removeSatisfied( clauses );

   unsigned k = 0 , cnt = 0;
   for( int i = 0 ; i < trail.size() ; ++ i )
   {
      if( var( trail[i]) >= (int)_nvar )
      {
         assert( assigns[ var( trail[i] ) ] == Minisat::l_True );
         assigns[ var( trail[i] ) ] = Minisat::l_Undef;
         cnt +=1 ;
      }
      else
      {
         trail[k++] = trail[i];
      }
   }
   if( cnt != NCTRLVAR ){ assert(false);exit(1);}
   assert( qhead == trail.size() );

   trail.shrink( trail.size() - k );
   qhead = k;
   _uctrl = 0;
}

